w:World. FairFifo  w-discrete-constraint(w) 

latex

Definitions	World, P  Q, A c B, P & Q, FairFifo, IdLnk, , Action(dec), w-action-dec(TA;M;i), , type List, {x:A| B(x)} , Msg(M), s = t, source(l), mlnk(m), w-automaton(T;TA;M), x:A. B(x), f(a), x:A  B(x), x:AB(x), Id, Type, , t  T, Top
Lemmas	top wf, bool wf, Id wf, w-automaton wf, mlnk wf, lsrc wf, Msg wf, nat wf, w-action-dec wf, action wf, rationals wf, IdLnk wf, fair-fifo wf